COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	declare INDCONST V V0 V1 V2 V3 ε variable
C00007 ENDMK
C⊗;
declare INDCONST V V0 V1 V2 V3 ε variable;
declare INDVAR v v0 v1 v2 v3 ε variable;

declare INDVAR u u0 u1 u2 u3 ε termform;
declare INDVAR p p0 p1 p2 p3 ε boolform;
declare INDVAR e e0 e1 e2 e3 ε environment;
declare INDVAR f f0 f1 f2 f3 ε functionform;
declare INDVAR c c0 c1 c2 c3 ε object;
declare INDVAR m m0 m1 m2 m3 ε manform;
declare INDCONST Mike Pat Joe John Mary mike pat joe john mary ε manform;

declare OPCONST value(termform,environment) = termform;
declare PREDCONST true(boolform);
declare PREDCONST nec(boolform);

axiom nec:	∀p.(nec p ⊃ true p);;

MOREGENERAL termform ≥ {manform,object,variable};

declare OPCONST all(variable,boolform) = boolform;
declare OPCONST exist(variable,boolform) = boolform;
DECLARE OPCONST and(boolform,boolform) = boolform [L←555,R←550];
DECLARE OPCONST or(boolform,boolform) = boolform [L←535,R←540];
DECLARE OPCONST implies(boolform,boolform) = boolform [L←515,R←520];
DECLARE OPCONST equiv(boolform,boolform) = boolform [L←505,R←510];
DECLARE OPCONST not(boolform) = boolform [R←575];

axiom and:	∀ p1 p2.(true(p1 and p2) ≡ true(p1) ∧ true(p2));;
axiom or:	∀ p1 p2 e.(true(p1 or p2,e) ≡ true(p1,e) ∨ true(p2,e));;
axiom implies:	∀ p1 p2 e.(true(p1 implies p2,e) ≡ (true(p1,e) ⊃ true(p2,e)));;
axiom equiv:	∀ p1 p2 e.(true(p1 equiv p2,e) ≡ (true(p1,e) ≡ true(p2,e)));;
axiom not:	∀p e.(true(not p,e) ≡ ¬true(p,e));;

DECLARE OPCONST equal(termform,termform) = boolform [L←600,R←605];

axiom equal:	∀u1 u2 e.(true(u1 equal u2,e) ≡ (value(u1,e) = value(u2,e)));;

declare OPCONST telephone(manform) = termform[R←610];

axiom telephone:	∀u e.(value(telephone m,e) = telephone value(m,e));;
			
declare OPCONST know(manform,termform) = boolform;
declare OPCONST k(manform,boolform) = boolform;
mark foo;
declare OPCONST subst(termform,variable,termform) = termform;
axiom subst:	∀v u.(subst(v,v,u) = u),
		∀v u.(subst(u,v,v) = u),
		∀v1 v2 u.(¬v1=v2 ⊃ subst(u,v1,v2) = v2)
		∀u v m.(subst(u,v,telephone m) = telephone subst(u,v,m))
		∀m p v u.(subst(u,v,k(m,p)) = k(subst(u,v,m),subst(u,v,p)))
		∀m u1 v u.2(subst(u1,v,know(m,u2))
			 = know(subst(u1,v,m),subst(u1,v,u2)))
;;

axiom know:	∀m1 m2 m e.true(know(m,telephone m1) and k(m,m1 equal m2)
			implies know(m,telephone m2),e)
		∀m u u1 u2.nec(k(m,u1 equal u2) implies
			k(m,subst(u1,v,u) equal subst(u2,v,u)))
		∀m u1 u2.nec(k(m,u1 equal u2) and know(m,u1) implies know(m,u2))
;;